package test;

import java.io.IOException;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import java.util.Random;

import util.Pair;
import dd.discrete.ADD;
import dd.discrete.ADD.ADDLeafOperation;
import dd.discrete.ADDDNode;
import dd.discrete.DD;

public class testThreshold {
	
	private static Random rand = new Random(0);

	private static Pair<ADD, ArrayList<String> > makeContext(int i) {
		ArrayList<String> order = new ArrayList<String>();
		
		for( int j = 0 ; j < i; ++j ){
			order.add(String.valueOf((char)('A'+j)));
		}
		
		return new Pair<ADD, ArrayList<String> >( new ADD(order), order );
		
	}
	
	public static int corresponds( int addValue, boolean exact , int threshvalue){
		if( exact ){
			if( addValue == threshvalue ){
				return 1;
			}else{
				return 0;
			}
		}else{
			if( addValue > threshvalue ){
				return 1;
			}else{
				return 0;
			}
		}
	}
	
	private static void verifyThreshold( final ADD context, final int add, final int bdd, final int threshvalue
			, final boolean exact){
		
		
		ADDLeafOperation leaf_op = new ADDLeafOperation(){

			@Override
			public void processADDLeaf(Map<Integer, Boolean> assign,
					double leaf_val) {
				
				int bddval = corresponds((int)leaf_val, exact, threshvalue);
				
				int BDD = bdd;
				
				for( Map.Entry<Integer, Boolean> entry : assign.entrySet() ){
					BDD = context.restrict(BDD, entry.getKey(), entry.getValue() ? DD.RESTRICT_HIGH : DD.RESTRICT_LOW );
				}
				
				assert( context.getNode(BDD) instanceof ADDDNode );
				
				if( ((ADDDNode)context.getNode(BDD))._dUpper != bddval ){
					System.err.println("threshold fail");
					context.getGraph(add).launchViewer();
					context.getGraph(bdd).launchViewer();
					try {
						System.in.read();
					} catch (IOException e) {
						e.printStackTrace();
					}
				}else{
					
				}
				
				
			}

			@Override
			public void processADDLeaf(ArrayList<String> assign, double leaf_val) {
			}

		};
		
		context.enumeratePaths(add, leaf_op, new HashMap<Integer, Boolean>());
		
		System.out.println("passed " + 
				context.countExactNodes(add) + " " 
				+ context.countExactNodes(bdd));
	}
	
	public static void main(String[] args) {
		//generate random ADD with leaf values in {-1,0,1}
		final int MAXVARS = 20;
		
		for( int i = 5; i < MAXVARS; ++i ){
			Pair<ADD, ArrayList<String>> inst = makeContext(i);
			int add = makeRandomADD(inst._o1, inst._o2, 0.75, 0,1,-1);
			int bdd = inst._o1.AddtoBdd(add, 0.0d, false);
			verifyThreshold(inst._o1, add, bdd, 0, false);
			 
			bdd = inst._o1.AddtoBdd(add, 0, true);
			verifyThreshold(inst._o1, add, bdd, 0, true);
		}
		//threshold exact at zero
		//threshold at zero
		
		//to verify 
		//traverse path in ADD till leaf
		//check corresponding value in BDD
		
		
	}
	
	private static int makeRandomADD(ADD context, List<String> order, 
			final double density, final int... vals) {
		//pick random variable
		//recurse
		//at leaf get random double
		return makeRandomADDInt(context, order, density, 0, vals);
	}

	private static int makeRandomADDInt(ADD context, List<String> vars, 
			final double density, int index, final int... vals) {
		if( index == vars.size() ){
			return context.getConstantNode( vals[rand .nextInt(vals.length)] );
		}
		
		if( Math.random() < density ){
			int high = makeRandomADDInt(context, vars, density, index+1, vals);
			int low = makeRandomADDInt(context, vars, density, index+1, vals);
			
			int id = (Integer)context._hmVarName2ID.get(vars.get(index));
			
			int lowbr = context.getVarNode(id, 1.0d, 0.0d);
			
			int highbr = context.getVarNode(id, 0.0d, 1.0d);

			low = context.applyInt(low, lowbr, DD.ARITH_PROD );
			high = context.applyInt(high, highbr, DD.ARITH_PROD );
			
			return context.applyInt(low, high, DD.ARITH_SUM );
		}
		return makeRandomADDInt(context, vars, density, index+1, vals);
	}
	
}
